/* Benchmarks for the PionterC verifier. */

// function call


/*@ i>=0
 */
int f(int i)
{
  return i;
}
/*@ result >= 0
 */



/*@ */
int main()
{
  int x;
  
  x = f(1);
  x = f(2);
  return x;
}
/*@ result >=0 */
